YES(O(1),O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { U11(tt(), M, N) -> U12(tt(), M, N)
  , U12(tt(), M, N) -> s(plus(N, M))
  , plus(N, s(M)) -> U11(tt(), M, N)
  , plus(N, 0()) -> N
  , U21(tt(), M, N) -> U22(tt(), M, N)
  , U22(tt(), M, N) -> plus(x(N, M), N)
  , x(N, s(M)) -> U21(tt(), M, N)
  , x(N, 0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs:
  { plus(N, s(M)) -> U11(tt(), M, N)
  , U22(tt(), M, N) -> plus(x(N, M), N) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  [U11](x1, x2, x3) = x1 + 2*x2 + x3                                                  
                                                                                      
             [tt]() = 1                                                               
                                                                                      
  [U12](x1, x2, x3) = x1 + 2*x2 + x3                                                  
                                                                                      
            [s](x1) = 1 + x1                                                          
                                                                                      
     [plus](x1, x2) = x1 + 2*x2                                                       
                                                                                      
  [U21](x1, x2, x3) = 2*x1 + 2*x1*x2 + 2*x1*x3 + 2*x1^2 + x2 + 2*x2*x3 + 2*x2^2 + 2*x3
                                                                                      
  [U22](x1, x2, x3) = 2*x1 + 2*x1*x3 + 2*x1^2 + 2*x2 + 2*x2*x3 + 2*x2^2 + 2*x3        
                                                                                      
        [x](x1, x2) = 2*x1 + 2*x1*x2 + 2*x2 + 2*x2^2                                  
                                                                                      
              [0]() = 0                                                               
                                                                                      
  
  This order satisfies the following ordering constraints.
  
    [U11(tt(), M, N)] =  1 + 2*M + N                  
                      >= 1 + 2*M + N                  
                      =  [U12(tt(), M, N)]            
                                                      
    [U12(tt(), M, N)] =  1 + 2*M + N                  
                      >= 1 + N + 2*M                  
                      =  [s(plus(N, M))]              
                                                      
      [plus(N, s(M))] =  N + 2 + 2*M                  
                      >  1 + 2*M + N                  
                      =  [U11(tt(), M, N)]            
                                                      
       [plus(N, 0())] =  N                            
                      >= N                            
                      =  [N]                          
                                                      
    [U21(tt(), M, N)] =  4 + 3*M + 4*N + 2*M*N + 2*M^2
                      >= 4 + 4*N + 2*M + 2*M*N + 2*M^2
                      =  [U22(tt(), M, N)]            
                                                      
    [U22(tt(), M, N)] =  4 + 4*N + 2*M + 2*M*N + 2*M^2
                      >  4*N + 2*N*M + 2*M + 2*M^2    
                      =  [plus(x(N, M), N)]           
                                                      
         [x(N, s(M))] =  4*N + 2*N*M + 4 + 6*M + 2*M^2
                      >= 4 + 3*M + 4*N + 2*M*N + 2*M^2
                      =  [U21(tt(), M, N)]            
                                                      
          [x(N, 0())] =  2*N                          
                      >=                              
                      =  [0()]                        
                                                      

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { U11(tt(), M, N) -> U12(tt(), M, N)
  , U12(tt(), M, N) -> s(plus(N, M))
  , plus(N, 0()) -> N
  , U21(tt(), M, N) -> U22(tt(), M, N)
  , x(N, s(M)) -> U21(tt(), M, N)
  , x(N, 0()) -> 0() }
Weak Trs:
  { plus(N, s(M)) -> U11(tt(), M, N)
  , U22(tt(), M, N) -> plus(x(N, M), N) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs: { x(N, s(M)) -> U21(tt(), M, N) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  [U11](x1, x2, x3) = 2*x1 + 2*x1*x2 + x2 + x3                  
                                                                
             [tt]() = 1                                         
                                                                
  [U12](x1, x2, x3) = 2*x1 + 3*x2 + x3                          
                                                                
            [s](x1) = 2 + x1                                    
                                                                
     [plus](x1, x2) = x1 + 3*x2                                 
                                                                
  [U21](x1, x2, x3) = x1 + 2*x1*x3 + 2*x2 + 2*x2*x3 + 2*x3      
                                                                
  [U22](x1, x2, x3) = x1 + x1*x2 + 2*x1*x3 + x2 + 2*x2*x3 + 2*x3
                                                                
        [x](x1, x2) = x1 + 2*x1*x2 + 2*x2                       
                                                                
              [0]() = 0                                         
                                                                
  
  This order satisfies the following ordering constraints.
  
    [U11(tt(), M, N)] =  2 + 3*M + N          
                      >= 2 + 3*M + N          
                      =  [U12(tt(), M, N)]    
                                              
    [U12(tt(), M, N)] =  2 + 3*M + N          
                      >= 2 + N + 3*M          
                      =  [s(plus(N, M))]      
                                              
      [plus(N, s(M))] =  N + 6 + 3*M          
                      >  2 + 3*M + N          
                      =  [U11(tt(), M, N)]    
                                              
       [plus(N, 0())] =  N                    
                      >= N                    
                      =  [N]                  
                                              
    [U21(tt(), M, N)] =  1 + 4*N + 2*M + 2*M*N
                      >= 1 + 2*M + 4*N + 2*M*N
                      =  [U22(tt(), M, N)]    
                                              
    [U22(tt(), M, N)] =  1 + 2*M + 4*N + 2*M*N
                      >  4*N + 2*N*M + 2*M    
                      =  [plus(x(N, M), N)]   
                                              
         [x(N, s(M))] =  5*N + 2*N*M + 4 + 2*M
                      >  1 + 4*N + 2*M + 2*M*N
                      =  [U21(tt(), M, N)]    
                                              
          [x(N, 0())] =  N                    
                      >=                      
                      =  [0()]                
                                              

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { U11(tt(), M, N) -> U12(tt(), M, N)
  , U12(tt(), M, N) -> s(plus(N, M))
  , plus(N, 0()) -> N
  , U21(tt(), M, N) -> U22(tt(), M, N)
  , x(N, 0()) -> 0() }
Weak Trs:
  { plus(N, s(M)) -> U11(tt(), M, N)
  , U22(tt(), M, N) -> plus(x(N, M), N)
  , x(N, s(M)) -> U21(tt(), M, N) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs:
  { plus(N, 0()) -> N
  , x(N, 0()) -> 0() }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  [U11](x1, x2, x3) = 1 + x1 + 2*x2 + x3                      
                                                              
             [tt]() = 1                                       
                                                              
  [U12](x1, x2, x3) = 1 + x1 + x1*x2 + x2 + x3                
                                                              
            [s](x1) = 2 + x1                                  
                                                              
     [plus](x1, x2) = x1 + 2*x2                               
                                                              
  [U21](x1, x2, x3) = x1 + x1*x2 + 2*x1*x3 + x2 + x2*x3 + 2*x3
                                                              
  [U22](x1, x2, x3) = x1 + x1*x2 + 2*x1*x3 + x2 + x2*x3 + 2*x3
                                                              
        [x](x1, x2) = 2*x1 + x1*x2 + 2*x2                     
                                                              
              [0]() = 1                                       
                                                              
  
  This order satisfies the following ordering constraints.
  
    [U11(tt(), M, N)] =  2 + 2*M + N        
                      >= 2 + 2*M + N        
                      =  [U12(tt(), M, N)]  
                                            
    [U12(tt(), M, N)] =  2 + 2*M + N        
                      >= 2 + N + 2*M        
                      =  [s(plus(N, M))]    
                                            
      [plus(N, s(M))] =  N + 4 + 2*M        
                      >  2 + 2*M + N        
                      =  [U11(tt(), M, N)]  
                                            
       [plus(N, 0())] =  N + 2              
                      >  N                  
                      =  [N]                
                                            
    [U21(tt(), M, N)] =  1 + 2*M + 4*N + M*N
                      >= 1 + 2*M + 4*N + M*N
                      =  [U22(tt(), M, N)]  
                                            
    [U22(tt(), M, N)] =  1 + 2*M + 4*N + M*N
                      >  4*N + N*M + 2*M    
                      =  [plus(x(N, M), N)] 
                                            
         [x(N, s(M))] =  4*N + N*M + 4 + 2*M
                      >  1 + 2*M + 4*N + M*N
                      =  [U21(tt(), M, N)]  
                                            
          [x(N, 0())] =  3*N + 2            
                      >  1                  
                      =  [0()]              
                                            

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { U11(tt(), M, N) -> U12(tt(), M, N)
  , U12(tt(), M, N) -> s(plus(N, M))
  , U21(tt(), M, N) -> U22(tt(), M, N) }
Weak Trs:
  { plus(N, s(M)) -> U11(tt(), M, N)
  , plus(N, 0()) -> N
  , U22(tt(), M, N) -> plus(x(N, M), N)
  , x(N, s(M)) -> U21(tt(), M, N)
  , x(N, 0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs:
  { U12(tt(), M, N) -> s(plus(N, M))
  , U21(tt(), M, N) -> U22(tt(), M, N) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  [U11](x1, x2, x3) = 2*x1 + 2*x2 + x3                          
                                                                
             [tt]() = 2                                         
                                                                
  [U12](x1, x2, x3) = 2*x1 + 2*x2 + x3                          
                                                                
            [s](x1) = 2 + x1                                    
                                                                
     [plus](x1, x2) = x1 + 2*x2                                 
                                                                
  [U21](x1, x2, x3) = 1 + 2*x1 + 2*x1*x3 + 2*x2 + 2*x2*x3 + 2*x3
                                                                
  [U22](x1, x2, x3) = 2*x1 + 2*x1*x3 + 2*x2 + 2*x2*x3 + x3      
                                                                
        [x](x1, x2) = 1 + 2*x1 + 2*x1*x2 + 2*x2                 
                                                                
              [0]() = 0                                         
                                                                
  
  This order satisfies the following ordering constraints.
  
    [U11(tt(), M, N)] =  4 + 2*M + N          
                      >= 4 + 2*M + N          
                      =  [U12(tt(), M, N)]    
                                              
    [U12(tt(), M, N)] =  4 + 2*M + N          
                      >  2 + N + 2*M          
                      =  [s(plus(N, M))]      
                                              
      [plus(N, s(M))] =  N + 4 + 2*M          
                      >= 4 + 2*M + N          
                      =  [U11(tt(), M, N)]    
                                              
       [plus(N, 0())] =  N                    
                      >= N                    
                      =  [N]                  
                                              
    [U21(tt(), M, N)] =  5 + 6*N + 2*M + 2*M*N
                      >  4 + 5*N + 2*M + 2*M*N
                      =  [U22(tt(), M, N)]    
                                              
    [U22(tt(), M, N)] =  4 + 5*N + 2*M + 2*M*N
                      >  1 + 4*N + 2*N*M + 2*M
                      =  [plus(x(N, M), N)]   
                                              
         [x(N, s(M))] =  5 + 6*N + 2*N*M + 2*M
                      >= 5 + 6*N + 2*M + 2*M*N
                      =  [U21(tt(), M, N)]    
                                              
          [x(N, 0())] =  1 + 2*N              
                      >                       
                      =  [0()]                
                                              

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs: { U11(tt(), M, N) -> U12(tt(), M, N) }
Weak Trs:
  { U12(tt(), M, N) -> s(plus(N, M))
  , plus(N, s(M)) -> U11(tt(), M, N)
  , plus(N, 0()) -> N
  , U21(tt(), M, N) -> U22(tt(), M, N)
  , U22(tt(), M, N) -> plus(x(N, M), N)
  , x(N, s(M)) -> U21(tt(), M, N)
  , x(N, 0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs: { U11(tt(), M, N) -> U12(tt(), M, N) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  [U11](x1, x2, x3) = 3 + x1 + 2*x2 + x3                                         
                                                                                 
             [tt]() = 1                                                          
                                                                                 
  [U12](x1, x2, x3) = x1 + 2*x1^2 + 2*x2 + x3                                    
                                                                                 
            [s](x1) = 1 + x1                                                     
                                                                                 
     [plus](x1, x2) = 2 + x1 + 2*x2                                              
                                                                                 
  [U21](x1, x2, x3) = 1 + x1 + 2*x1*x2 + 2*x1*x3 + 2*x2 + 2*x2*x3 + 2*x2^2 + 2*x3
                                                                                 
  [U22](x1, x2, x3) = 1 + x1 + 2*x1*x2 + x1*x3 + x2 + 2*x2*x3 + 2*x2^2 + 3*x3    
                                                                                 
        [x](x1, x2) = 2*x1 + 2*x1*x2 + 2*x2 + 2*x2^2                             
                                                                                 
              [0]() = 0                                                          
                                                                                 
  
  This order satisfies the following ordering constraints.
  
    [U11(tt(), M, N)] =  4 + 2*M + N                  
                      >  3 + 2*M + N                  
                      =  [U12(tt(), M, N)]            
                                                      
    [U12(tt(), M, N)] =  3 + 2*M + N                  
                      >= 3 + N + 2*M                  
                      =  [s(plus(N, M))]              
                                                      
      [plus(N, s(M))] =  4 + N + 2*M                  
                      >= 4 + 2*M + N                  
                      =  [U11(tt(), M, N)]            
                                                      
       [plus(N, 0())] =  2 + N                        
                      >  N                            
                      =  [N]                          
                                                      
    [U21(tt(), M, N)] =  2 + 4*M + 4*N + 2*M*N + 2*M^2
                      >= 2 + 3*M + 4*N + 2*M*N + 2*M^2
                      =  [U22(tt(), M, N)]            
                                                      
    [U22(tt(), M, N)] =  2 + 3*M + 4*N + 2*M*N + 2*M^2
                      >= 2 + 4*N + 2*N*M + 2*M + 2*M^2
                      =  [plus(x(N, M), N)]           
                                                      
         [x(N, s(M))] =  4*N + 2*N*M + 4 + 6*M + 2*M^2
                      >  2 + 4*M + 4*N + 2*M*N + 2*M^2
                      =  [U21(tt(), M, N)]            
                                                      
          [x(N, 0())] =  2*N                          
                      >=                              
                      =  [0()]                        
                                                      

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { U11(tt(), M, N) -> U12(tt(), M, N)
  , U12(tt(), M, N) -> s(plus(N, M))
  , plus(N, s(M)) -> U11(tt(), M, N)
  , plus(N, 0()) -> N
  , U21(tt(), M, N) -> U22(tt(), M, N)
  , U22(tt(), M, N) -> plus(x(N, M), N)
  , x(N, s(M)) -> U21(tt(), M, N)
  , x(N, 0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^2))